$\forall$${\it the\_es}$:ES, $j$:E.
\\[0ex]isrcv($j$)
\\[0ex]$\Rightarrow$ snds(lnk($j$), before(sender($j$),index($j$))) $=$ nil $\in$ (Msg on lnk($j$)) List
\\[0ex]$\Rightarrow$ msgs(lnk($j$);before($j$)) $=$ nil $\in$ Msg List